Skip to content

UnivMon: certify L2 from layer 0's F2 - #621

Closed
zzylol wants to merge 2 commits into
stack/editor-sqlfrom
stack/univmon-l2-accuracy
Closed

UnivMon: certify L2 from layer 0's F2#621
zzylol wants to merge 2 commits into
stack/editor-sqlfrom
stack/univmon-l2-accuracy

Conversation

@zzylol

@zzylol zzylol commented Oct 5, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

Stack: #574 → #620 → #618 → #621 → #627 → #625 → #628 → #632 → #634 → #616 → #617 → #622 → #624 → #629 → #630 → #631 → #633 → #635 → #636 → #637

Problem

Stage 3 rejected every UnivMon candidate ("no accuracy model for UnivMon"). The only certified readout was the exact total. The kernel read L2 via calc_l2, the square root of the heavy-hitter G-sum heuristic, and no theory covers that readout. UnivMon's shape was a fixed 5×1024×16 whatever the requirement, and Stage 3 priced it through the catch-all (1, 1_024).

Changes

  • Executor: FrequencyL2 now reads l2_sketch_layers[0].get_l2(). That is √(median over rows of Σ C²) on layer 0, which sees the whole stream. It is the textbook AMS F₂ estimator and is linear under merge. No sketchlib change.
  • Guarantee (estimators/univmon.rs): FrequencyL2 is now certified.
    • Per row, Chebyshev with p = 0.1 gives ε₂ = √(20/w), since Var[R] ≤ 2F₂²/w.
    • The median of d odd rows fails with probability at most the binomial tail Σ_{i≥(d+1)/2} C(d,i)pⁱ(1−p)^(d−i).
    • The L2 bound is 1 − √(1 − ε₂), the lower side. The upper side √(1+ε₂) − 1 is smaller.
    • Reported as RelativeValue under contract univmon_layer0_f2_median_chebyshev_v1. The contract records the idealized 128-bit-hash assumption, p and the readout.
    • Fails closed (None) unless d is odd, w is a power of two and d·log₂w + d ≤ 128. sketchlib slices each row's column and sign from one 128-bit hash, so outside these conditions the rows are not independent.
    • Distinct count and entropy stay uncertified. The total stays exact.
  • Sizing: depends only on (ε, δ), not on the intent, so Pass 2's capability sharing still gives identical states.
    • d is the smallest odd depth whose tail is ≤ δ, capped at 19 because the executor's kernel rejects more than 20 rows.
    • w is the next power of two ≥ 20/(2ε−ε²)².
    • Heap stays 256 and layers stay 16.
    • Shapes past the bit budget are kept, and the guarantee rejects them. For example (0.01, 0.001) gives 9×2¹⁶ and is rejected.
    • With no positive ε (the exact-count alternative, which reads only the exact total) the old 5×1024 baseline is kept.
  • Stage 3 pricing: summary_shape gets a UnivMon arm. Ops per row are 2·(2d + 4), since an insert reaches about 2 layers. State bytes come from Pass 1's sketch_state_bytes.
  • Tests:
    • univmon.rs units: L2 certified at (0.01, 0.01) with RelativeValue; even d, non-power-of-two w and bit-budget overflow give None; tighter ε/δ give more columns/rows; F0 and entropy stay None.
    • Executor: the readout equals layer-0 get_l2, and on a Zipf(1) stream at the (0.01, 0.01) sizing it is within 1% of the true L2.
    • plan-selection: Example 2's Q3 UnivMon passes build_violation, while Q1 and Q2 still fail with "no accuracy model".
  • Tests changed by side effects of this PR:
    • frontend-promql/tests/univmon_candidates.rs: count now uses the same ε as the other three readouts, so all four share one shape. L2 is now expected to be certified, and the "uncalibrated" test covers entropy only.
    • integration-tests/tests/precompute_raw_samples.rs: raises this test's executor max_bytes to 1 GiB. A UnivMon sized at ε = 0.02 is about 10 MiB per population (16 layers × 5 × 2¹⁴ × 8 B), so five series exceed the default 64 MiB.
    • planner/tests/summary_sharing.rs (stage-pipeline sharing test): with synthetic evidence, the plan whose three estimates read one UnivMon build is valid. It is no longer selected, because the new pricing (28 updates/row) costs more than exact counting. The test now asserts that the valid shared candidate exists.
  • Docs: accuracy-models.md table row and univmon-frequency-summary.md updated. Doc comments updated in devtools/tests/stage_pipeline.rs and summary_sharing.rs.

Example 2 (stage_pipeline --example planner-layering-2):

  • Before and after, the selection is the same: P86 "Q1 exact · Q2 exact (Count acc) · Q3 exact (Count acc) · shared summary", at 0.02367 cost/s.
  • Valid candidates go from 8 to 16. The 8 new ones use UnivMon for Q3.
  • The cheapest UnivMon plan is P88, "Q1 exact · Q2 exact (Count acc) · Q3 UnivMon (Count acc) · shared summary", at 0.06867 cost/s.
  • tools/dag-viewer/examples/planner-layering-example1.json is unchanged (the fixture test passes).
  • fix: integrate with fix(pass1): offer no per-group sketch for SQL COUNT(*) #620: fix(pass1): offer no per-group sketch for SQL COUNT(*) #620 requires every priced Stage 3 candidate to bind. With L2 certified, Example 2's UnivMon over src_ip (a unit-weight item update) is now priced, but the executor's physical planner sent it to the keyed weighted-frequency build, which has no UnivMon kernel. It now binds as UnivMon's value-frequency build over the item column, which already counts typed SQL identities (priced_example2_candidates_bind).

Test plan

  • cargo fmt --all --check
  • cargo clippy --workspace --all-targets -- -D warnings
  • cargo test --workspace: 1677 passed, 0 failed, 21 ignored (re-run after the rebase on main d4869a7)

@zzylol zzylol mentioned this pull request Oct 5, 2026
Closed
3 tasks done
@zzylol
zzylol force-pushed the stack/univmon-l2-accuracy branch from 18cb590 to ba716f2 Compare October 5, 2026 03:07
@zzylol
zzylol changed the base branch from stack/509-viewer-stages to stack/editor-sql October 5, 2026 03:08
This was referenced Oct 5, 2026
Closed
Draft
Closed
Draft
Draft
Draft
Draft
Draft
Closed
Closed
Draft
@zzylol
zzylol force-pushed the stack/univmon-l2-accuracy branch from ba716f2 to e34c85c Compare October 5, 2026 06:21
This was referenced Oct 5, 2026
Closed
Draft
Closed
Draft
Draft
Draft
Draft
Closed
Draft
Draft
@zzylol
zzylol force-pushed the stack/univmon-l2-accuracy branch 2 times, most recently from 165a3fa to d6d7d6b Compare October 10, 2026 14:32
zzylol and others added 2 commits October 11, 2026 16:22
@zzylol @claude
feat(accuracy): certify UnivMon L2 from layer 0's F2
1f90388 
UnivMon's L2 readout now reads layer 0's CountSketch row-median F2
(the textbook AMS estimator over the whole stream) instead of the
heavy-hitter G-sum heuristic, and the built-in model certifies it:
Chebyshev per row (p = 0.1, eps2 = sqrt(20/w)), binomial median tail
over odd d rows, relative L2 bound 1 - sqrt(1 - eps2). Fails closed
unless d is odd, w a power of two and d*log2(w) + d <= 128. UnivMon is
sized by inverting that bound for every readout, and Stage 3 prices it
from its rows and Pass 1's state-size function.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@zzylol @claude
fix: integrate with #620
011d946 
#620's priced_example2_candidates_bind requires every priced Stage 3
candidate to bind. With UnivMon L2 certified, Example 2's UnivMon over
src_ip (unit-weight item update) is now priced, but the physical planner
sent it to the keyed weighted-frequency build, which has no UnivMon
kernel. Bind it as UnivMon's value-frequency build over the item column,
which already counts typed SQL identities.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@zzylol
zzylol force-pushed the stack/univmon-l2-accuracy branch from d6d7d6b to 011d946 Compare October 11, 2026 17:11
zzylol added a commit that referenced this pull request Oct 13, 2026
@zzylol @claude
test: port #590's Example 2-4 acceptance specs and tests
a75cf7a 
The specs and tests from #590 run the current stages through the shared
planner_layering_common pipeline (Pass 1 and composition,
optimize_physical_asap, select_plan); tests are named after the stages.
Materialization is read from the physical DAG (#667); window forms and
retention stay pending adapters. Behavior that works passes (29 tests);
every expectation that needs a feature not in this stack is ignored with
the PR that delivers it (29 tests): Pass 2 sharing (#588, #595, #596),
window composition (#601, #628, #634), materialization enumeration and
MatAtQuery (#604, #625), UnivMon sizing and accuracy (#621), SQL
recognition and COUNT(*) composition (#598, #603) and plan selection row
estimates (#632). Each spec's "Today" column states the current output.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW
@zzylol zzylol mentioned this pull request Oct 13, 2026
Merged
3 tasks
zzylol added a commit that referenced this pull request Oct 13, 2026
@zzylol @claude
test: port #590's Example 2-4 acceptance specs and tests
3f5174f 
The specs and tests from #590 run the current stages through the shared
planner_layering_common pipeline (Pass 1 and composition,
optimize_physical_asap, select_plan); tests are named after the stages.
Materialization is read from the physical DAG (#667); window forms and
retention stay pending adapters. Behavior that works passes (29 tests);
every expectation that needs a feature not in this stack is ignored with
the PR that delivers it (29 tests): Pass 2 sharing (#588, #595, #596),
window composition (#601, #628, #634), materialization enumeration and
MatAtQuery (#604, #625), UnivMon sizing and accuracy (#621), SQL
recognition and COUNT(*) composition (#598, #603) and plan selection row
estimates (#632). Each spec's "Today" column states the current output.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW
zzylol added a commit that referenced this pull request Oct 13, 2026
@zzylol @claude
test: planner-layering Examples 1–4 acceptance specs on the planning …
fa65f46 
…stages (#577)

* test: acceptance spec and pending tests for planner-layering Example 1

Define MVP acceptance for #509 Example 1 before the Phase C stage APIs
exist: 1 -> 6 -> 6 -> 1 candidates (Pass 1 x identical-expression
sharing; physical operator implementation only, no materialization).

- Spec with per-stage candidate tables, invariants and doc ambiguities.
- Integration tests against todo!() stage stubs, ignored until the
  stages land; workload and Stage 0 frontend-shape tests run now.
- Expected-only asap-stage-pipeline/v1 fixture for the DAG viewer.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

* test: run the Example 1 acceptance tests against the real stages

Replace the todo!() stubs with adapters over Stage 0-3, un-ignore the 11
tests that pass, and give each still-ignored test the precise difference
between the implementation and the spec. Add runtime capability checks:
the selected plan compiles in the physical planner; compiling every
candidate stays ignored with the two runtime gaps it finds.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

* test: read Example 1 logical stages as flat DAGs after the export removal

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* test: Example 1 acceptance on the composed stages (1 -> 3 -> 3 -> 1)

The tests run Pass 1 and composition, optimize_physical_asap and
select_plan through a shared tests/planner_layering_common pipeline, and
follow the decided behavior: three Pass 1 candidates (Q2 exact, CMS+heap,
CountSketch+heap), every sub-DAG NotMaterialized, P1 selected, CMS+heap
invalid (weights not proven non-negative) and CountSketch+heap invalid (a
Top-K output has no guarantee and no deployment evidence). Hydra (#605),
Pass 2 sharing (#588) and the two runtime gaps (#593, #579) stay ignored
with the PR that delivers them. Tests are named after the stages; the
compile check no longer uses the PromQL fallback. The spec lists where the
doc and the planner differ. The expected-only viewer fixture is removed:
the generated four-stage fixture replaces it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* test: port #590's Example 2-4 acceptance specs and tests

The specs and tests from #590 run the current stages through the shared
planner_layering_common pipeline (Pass 1 and composition,
optimize_physical_asap, select_plan); tests are named after the stages.
Materialization is read from the physical DAG (#667); window forms and
retention stay pending adapters. Behavior that works passes (29 tests);
every expectation that needs a feature not in this stack is ignored with
the PR that delivers it (29 tests): Pass 2 sharing (#588, #595, #596),
window composition (#601, #628, #634), materialization enumeration and
MatAtQuery (#604, #625), UnivMon sizing and accuracy (#621), SQL
recognition and COUNT(*) composition (#598, #603) and plan selection row
estimates (#632). Each spec's "Today" column states the current output.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* feat(devtools): stage_pipeline examples for #509 Example 3

Ported from #590: --example planner-layering-3a (Pattern A, ad hoc batch of
five p99 reports) and planner-layering-3b (Pattern B, repeating 5-min p99),
the Example 3 acceptance tests' workloads. Example 1's output is unchanged.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* test: follow #576's per-consumer charging and exact top-k columns

Plan selection charges a NotMaterialized node once per consuming query,
so the charging helper checks NodeCost.multiplier and the Example 4 A3
ambiguity is recorded as decided. Example 1 checks that exact Q2 sorts by
the ranked value and returns [job, topk_10]. The stage viewer guide's
tab 1 row now describes the actual all-exact result.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* refactor(devtools): one planning pipeline for stage_pipeline and the acceptance tests

run_planning_stages and the #509 example workloads move into the
asap-devtools library; stage_pipeline serializes the run and the
planner-layering tests adapt it. The shared data workload drops
ingestion_rate for data at rest, which validate() requires.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* fix(devtools): select over every candidate; --max-displayed limits only the document

stage_pipeline capped enumeration at 64, so Example 3a (243 candidates)
selected P41 instead of the cheapest P122 (KLL for all five queries).
The pipeline now enumerates, optimizes and prices every candidate; the
document shows the first --max-displayed (default 64) plus the selected
one, with `combinations` and `capped`.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* docs: Example 2's SQL candidates compose; the SQL test waits only on #598

Running the ignored SQL test composes every candidate and fails only on
Q2's options (per-source counts until #598), so #603 is not a blocker.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* test: name stages by number and name; say query-language frontends

The frontends' Run field, id and locals become stage0_query_language_frontends,
and test names carry stage0..stage3 with the stage name.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* test: charging helper follows plan selection's per-consumer rule

With a materialized node the helper accepted any multiplier >= 1. It now
computes each node's computations as plan selection does (walks from
query roots and materialized nodes' inputs, stopping at materialized
nodes), checked on a hand-built candidate with a materialized node.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* test: Example 1 picks Q2 candidates by (option, no shared input)

physical_with and the invalid-candidate check no longer assume one
candidate per Q2 option, so #588's shared-input variants need no change.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* docs: Example 3 Pattern B charges each node once per consuming query

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* docs(stage-viewer): rows 2, 3a and 3b describe the planner's current output

Read from uncapped runs: Example 2's sketch plans are rejected for having
no (ε, δ) guarantee, 3a selects P122 (first of 108 tied cheapest plans,
nothing shared yet) and 3b selects query-time KLL; panes and the latency
check come with the window-summary PRs.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* docs(stage-viewer): row 2 from the SQL run; 3a ties 32 plans, not 108

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* test: Example 1 counts only unshared candidates; stage3_ charging-helper names

The 3-logical and 3-physical counts now hold when #588 adds shared-input
variants.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* refactor(devtools): PlanningStagesRun fields carry stage number and name

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

* test(devtools): unique temp file per stage_pipeline run

cargo test runs the tests as threads of one process, so two runs of the same
example shared a file name and one deleted the other's output.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01W7qG9aFyPij5uWsyAJCxDW

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This was referenced Oct 13, 2026
Open
Merged
Merged
@zzylol

zzylol commented Oct 15, 2026

Copy link
Copy Markdown
Contributor Author

Superseded by #707 (merged): G5, Example 2 — Pass 2 summary-capability rule, UnivMon, SQL L2/entropy idioms.

@zzylol zzylol closed this Oct 15, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@zzylol